| Definitions | A c B,  x:A. B(x), P  Q, i <z j,   b, i  z j, nth_tl(n;as), hd(l), A B, i j < k, ||as||, {i..j }, l[i], {T}, SQType(T), P & Q, Top,  , False, True, if b then t else f fi , Y, reduce(f;k;as), deq-member(eq;x;L), tt, ff, t.1,  ,   x. t(x), t  T, MaName, R-names(A), R-loc(R), Rds(R), x dom(f), Rnone?(x1), Rplus?(x1),  b, A, P   Q,  x:A. B(x), Dec(P), P  Q, P Q, x(s), Unit, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, Rnone(),  , fpf-domain(f) |